w:World, e, e':E. FairFifo  loc(e) = loc(e')  Id  (e < e'  time(e)<time(e')) 

latex

Definitions	x:A. B(x), P  Q, P  Q, e < e', R^+, x:A. B(x), x f y, P & Q, P  Q, t  T, Prop, rel_exp(T;R;n), , AB, A, False, SQType(T), {T}, Y, if b t else f fi, i=j, false, true, , Dec(P), P  Q, , Unit, S  T,
Lemmas	nat plus wf, rel exp wf, nat plus inc, pred! wf, w-info wf, w-pred wf, w-time wf, nat wf, Id wf, loc wf, w-E wf, fair-fifo wf, world wf, nat plus properties, le wf, decidable int equal, w-pred!-decreases, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff